| Definitions | E, WellFnd{i}(A;x,y.R(x;y)), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), tag(k), msg(l;t;v), tl(l), i< j,  b, i j, if b t else f fi, nth_tl(n;as), hd(l), l[i], Trans x,y:T. E(x;y), ESAxioms(E;T;M;loc;kind;val;when;after;sends;sender;index;first;pred;causl), outl(x), lnk(k), Y, ||as||, AB, i j < k, {i..j }, isl(x), isrcv(k), mlnk(m), haslink(l;m), Msg(M), Msg_sub(l;M), Knd, Top, t  T, Unit,  , EqDecider(T), ES, 2of(t), 1of(t), (e < e'), A,  x:A. B(x), Prop, P   Q, {T},  x. t(x), False |